Nuprl Lemma : dsys-sub-join-left
11,40
postcript
pdf
A
,
B
:Dsys.
A
A
B
latex
Definitions
x
:
A
.
B
(
x
)
,
D1
D2
,
A
B
,
M(
i
)
,
t
T
,
Dsys
Lemmas
ma-sub-join-left
,
Id
wf
,
dsys
wf
origin
A, B:Dsys. A 
A 
B A, B:Dsys. A A B x:A. B(x) D2 B
T